i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{k:Knd| 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{(k  ks)} 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(decl-state(ds)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(ma-valtype(da; k)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(TT).
((fpf-dom(id-deq; x; ds)))
 (A:es_realizer{i:l}. 
 R-Feasible{i:l}
 R-Feasible(A)
  ((R-has-loc(A; i)))
  l_all(ks;
  l_all(Knd;
  l_all(k.((isrcv(k))
  l_all( subtype_rel(fpf-cap(R-da(A; source(lnk(k))); Kind-deq; k; void); ma-valtype(da; k))))
  l_all(ks; Knd; k.(fpf-dom(Kind-deq; k; da)))
  R-compat{i:l}
  R-compat(R-state-var(i; ds; da; x; T; ks; tr); A)) 

latex

Definitions

P  Q, True, T, x(s), P  Q, P  Q, Id, A, x. t(x), top, prop{i:l}, t  T, l_all(L; T; x.P(x)), es_realizer{i:l}, P  Q, Knd, fpf(A; a.B(a)), x:A. B(x), False

Lemmas

read-restricted wf, read-restricted-has-loc, write-restricted wf, write-restricted-has-loc, not-R-has-loc-R-da, fpf-empty-compatible-right, not-R-has-loc-R-ds, deq wf, true wf, squash wf, fpf-compatible wf, R-occurs wf, R-occurs-has-loc, Id wf, id-deq wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, rationals wf, unit wf, R-Feasible wf, R-has-loc wf, not wf, ma-valtype wf, lnk wf, lsrc wf, R-da wf, fpf-cap wf, isrcv wf, Knd wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-single wf, top wf, fpf-join wf, fpf-dom wf, assert wf, IdLnk wf, l member wf, R-state-var-compat